A,B:Type, a:EqDecider(A), b:EqDecider(B). product-deq(A; B; a; b)  EqDecider(:A  B) 

latex

Definitions

s = t, strong-subtype(A; B), x:AB(x), P  Q, x:A. B(x), x:A  B(x), Type, EqDecider(T), b, axiom, t  T, prop{i:l}, proddeq(a; b), f(a), P  Q, P  Q, P  Q, x.A(x), <a, b>, product-deq(A; B; a; b), Unit, False, , void, A, ff, , b, True, eq_bool(p; q), i <z j, i z j, (i = j), eq_atom(x; y), null(as), set_blt(p; a; b), set_le(p), x f y, set_eq(p), grp_blt(g; a; b), grp_eq(g), rng_eq(r), dcdr-to-bool(d), eq_atom{$n:n}(x; y), q_le(r; s), q_less(a; b), qeq(r; s), bimplies(p; q), band(p; q), bor(p; q), tt, , left + right, p-outcome(p), #$n, case b of inl(x) => s(x) | inr(y) => t(y), if b then t else f fi , t.2, t.1, x. t(x)

Lemmas

assert of band, pi2 wf, pi1 wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, true wf, bool wf, bnot wf, not wf, it wf, false wf, unit wf, subtype rel wf, deq wf, proddeq wf, iff wf, assert wf, member wf